k:, p:FinProbSpace, n:, X:({0..k}RandomVariable(p;n)).
E(n;s.0  i < k. X(i,s)) = 0  i < k. E(n;X(i))   

latex

Definitions

FinProbSpace, t  T, x:A. B(x), , RandomVariable(p;n), #$n, {i..j}, Type, x:AB(x), a  j < b. E(j), E(n;F), <a, b>, , s = t, P  Q, False, A, A  B, , {x:A| B(x)} , i  j , -n, n+m, n - m, a < b, Void, Outcome, f(a), x.A(x), , True, b, b, i z j, , i <z j, T, P  Q, x:A  B(x), P & Q, P  Q, Unit, left + right, 0, <+*>, +r, e, r+gp, *,  lb  i < ub. E(i), (r) i  k < j. E(k), r + s, s ~ t, x f y, X + Y, i  j < k, x. t(x), ||as||, S  T, suptype(S; T)

Lemmas

int-rational, length wf1, expectation-rv-add, rationals wf, qadd wf, qsum wf, expectation wf, eqtt to assert, assert of lt int, iff transitivity, eqff to assert, squash wf, true wf, bnot of lt int, assert of le int, lt int wf, bool wf, le int wf, le wf, assert wf, bnot wf, expectation-constant, p-outcome wf, int inc rationals, ge wf, nat properties, int seg wf, random-variable wf, nat wf, finite-prob-space wf